$\forall$${\it the\_es}$:event\_system\{i:l\}. es{-}Msg(${\it the\_es}$) $\in$ Type